workspace: Adapt to mutter API changes

diff --git a/js/ui/workspace.js b/js/ui/workspace.js
index 75683ba6577ebb66a2f9bbfaaa91cc28f035475a..7bd153bee26510e2abb045509683f43770b867a7 100644 (file)
--- a/js/ui/workspace.js
+++ b/js/ui/workspace.js
@@ -1621,9 +1621,7 @@ const Workspace = new Lang.Class({
                 metaWindow.move_to_monitor(this.monitorIndex);
 
             let index = this.metaWorkspace ? this.metaWorkspace.index() : global.screen.get_active_workspace_index();
-            metaWindow.change_workspace_by_index(index,
-                                                 false, // don't create workspace
-                                                 time);
+            metaWindow.change_workspace_by_index(index, false);
             return true;
         } else if (source.shellWorkspaceLaunch) {
             source.shellWorkspaceLaunch({ workspace: this.metaWorkspace ? this.metaWorkspace.index() : -1,

diff --git a/js/ui/workspaceThumbnail.js b/js/ui/workspaceThumbnail.js
index 210445bc464e06b88fe004bf6f5ea9305487e023..9dbc1afda3e737bc29e506cf89d3b0c9640a1c22 100644 (file)
--- a/js/ui/workspaceThumbnail.js
+++ b/js/ui/workspaceThumbnail.js
@@ -507,9 +507,7 @@ const WorkspaceThumbnail = new Lang.Class({
             if (metaWindow.get_monitor() != this.monitorIndex)
                 metaWindow.move_to_monitor(this.monitorIndex);
 
-            metaWindow.change_workspace_by_index(this.metaWorkspace.index(),
-                                                 false, // don't create workspace
-                                                 time);
+            metaWindow.change_workspace_by_index(this.metaWorkspace.index(), false);
             return true;
         } else if (source.shellWorkspaceLaunch) {
             source.shellWorkspaceLaunch({ workspace: this.metaWorkspace ? this.metaWorkspace.index() : -1,
@@ -739,14 +737,12 @@ const ThumbnailsBox = new Lang.Class({
 
             // ... move them down one.
             windows.forEach(function(win) {
-                win.meta_window.change_workspace_by_index(win.get_workspace() + 1,
-                                                          true, time);
+                win.meta_window.change_workspace_by_index(win.get_workspace() + 1, true);
             });
 
             if (isWindow)
                 // ... and bam, a workspace, good as new.
-                source.metaWindow.change_workspace_by_index(newWorkspaceIndex,
-                                                            true, time);
+                source.metaWindow.change_workspace_by_index(newWorkspaceIndex, true);
             else if (source.shellWorkspaceLaunch) {
                 source.shellWorkspaceLaunch({ workspace: newWorkspaceIndex,
                                               timestamp: time });